MacroNotToTerm.agda:11,3-10
Result type of a macro must be Term → TC ⊤
